Parity game
A parity game is played on a colored directed graph, where each node has been colored by a priority – one of (usually) finitely many natural numbers. Two players, 0 and 1, take turns moving a token along the edges of the graph, resulting in a (possibly infinite) path, called the play.
The winner of a finite play is the player whose opponent is unable to move. The winner of an infinite play is determined by the priorities appearing in the play. Typically, player 0 wins an infinite play if the smallest priority that occurs infinitely often in the play is even. Player 1 wins otherwise. This explains the word "parity" in the title.
Parity games lie in the third level of the borel hierarchy, and are consequently determined[1].
Games related to parity games were implicitly used in Rabin's proof of decidability of second order theory of n successors, where determinacy of such games was proven[2]. The Knaster–Tarski theorem leads to a relatively simple proof of determinacy of parity games[3].
Moreover, parity games are history-free determined[3][4][5]. This means that if a player has a winning strategy then she has a winning strategy that depends only on the current board position, and not on the history of the play.
Contents |
Solving a game
| Can parity games be solved in polynomial time? |
Solving a parity game played on a finite graph means deciding, for a given starting position, which of the two players has a winning strategy. It has been shown that this problem is in NP and Co-NP, as well as UP and co-UP.[6] It remains an open question whether this decision problem is solvable in PTime.
Given that parity games are history-free determined, solving a given parity game is equivalent to solving the following simple looking graph-theoretic problem. Given a finite colored directed bipartite graph with n vertices 
, and V colored with colors from 1 to m, is there a choice function selecting a single out-going edge from each vertex of 
, such that the resulting subgraph has the property that in each cycle the smallest occurring color is even.
Related games and their decision problems
A slight modification of the above game, and the related graph-theoretic problem, makes solving the game NP-hard. The modified game has the Rabin acceptance condition. Specifically, in the above bipartite graph scenario, the problem now is to determine if there is a choice function selecting a single out-going edge from each vertex of V0, such that the resulting subgraph has the property that in each cycle (and hence each strongly connected component) it is the case that there exists an i and a node with color 2i, and no node with color 2i − 1..
Note that as opposed to parity games, this game is no longer symmetric with respect to players 0 and 1.
Relation with logic and automata theory
References
- ^ D. A. Martin: Borel determinacy, The Annals of Mathematics, Vol 102 No. 2 pp. 363–371 (1975)
- ^ Rabin, MO (1969). "Decidability of second order theories and automata on infinite trees". Trans. AMS (American Mathematical Society) 141: 1–35. doi:10.2307/1995086. JSTOR 1995086.
- ^ a b E. A. Emerson and C. S. Jutla: Tree Automata, Mu-Calculus and Determinacy, IEEE Proc. Foundations of Computer Science, pp 368–377 (1991), ISBN 0-8186-2445-0
- ^ A. Mostowski: Games with forbidden positions, University of Gdansk, Tech. Report 78 (1991)
- ^ Zielonka, W (1998). "Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees". Theor. Comput. Sci. 200 (1–2): 135–183. doi:10.1016/S0304-3975(98)00009-7.
- ^ Grädel 2007, p. 163
- Erich Grädel, Phokion G. Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema, Scott Weinstein (2007). Finite model theory and its applications. Springer. ISBN 9783540004288.
Further reading
- E. Grädel, W. Thomas, T. Wilke (Eds.) : Automata, Logics, and Infinite Games, Springer LNCS 2500 (2003), ISBN 3540003886
External links
Parity Game Solvers: